Search Results

Documents authored by Birkedal, Lars

Document
DOI: 10.4230/LIPIcs.CSL.2024.47
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics

Authors: Jonathan Sterling, Daniel Gratzer, and Lars Birkedal

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky’s univalent foundations. We observe for the first time the profound impact of univalence on the denotational semantics of mutable state. Univalence automatically ensures that all computations are invariant under symmetries of the heap - a bountiful source of program equivalences. In particular, even the most simplistic univalent model enjoys many new equations that do not hold when the same constructions are carried out in the universes of traditional set-level (extensional) type theory.
Cite as

Jonathan Sterling, Daniel Gratzer, and Lars Birkedal. Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 47:1-47:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{sterling_et_al:LIPIcs.CSL.2024.47,
  author =	{Sterling, Jonathan and Gratzer, Daniel and Birkedal, Lars},
  title =	{{Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{47:1--47:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.47},
  URN =		{urn:nbn:de:0030-drops-196901},
  doi =		{10.4230/LIPIcs.CSL.2024.47},
  annote =	{Keywords: univalent foundations, homotopy type theory, impredicative encodings, synthetic guarded domain theory, guarded recursion, higher-order store, reference types}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.6
{mitten}: A Flexible Multimodal Proof Assistant

Authors: Philipp Stassen, Daniel Gratzer, and Lars Birkedal

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
Recently, there has been a growing interest in type theories which include modalities, unary type constructors which need not commute with substitution. Here we focus on MTT [Daniel Gratzer et al., 2021], a general modal type theory which can internalize arbitrary collections of (dependent) right adjoints [Birkedal et al., 2020]. These modalities are specified by mode theories [Licata and Shulman, 2016], 2-categories whose objects corresponds to modes, morphisms to modalities, and 2-cells to natural transformations between modalities. We contribute a defunctionalized NbE algorithm which reduces the type-checking problem for MTT to deciding the word problem for the mode theory. The algorithm is restricted to the class of preordered mode theories - mode theories with at most one 2-cell between any pair of modalities. Crucially, the normalization algorithm does not depend on the particulars of the mode theory and can be applied without change to any preordered collection of modalities. Furthermore, we specify a bidirectional syntax for MTT together with a type-checking algorithm. We further contribute mitten, a flexible experimental proof assistant implementing these algorithms which supports all decidable preordered mode theories without alteration.
Cite as

Philipp Stassen, Daniel Gratzer, and Lars Birkedal. {mitten}: A Flexible Multimodal Proof Assistant. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{stassen_et_al:LIPIcs.TYPES.2022.6,
  author =	{Stassen, Philipp and Gratzer, Daniel and Birkedal, Lars},
  title =	{{\{mitten\}: A Flexible Multimodal Proof Assistant}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.6},
  URN =		{urn:nbn:de:0030-drops-184498},
  doi =		{10.4230/LIPIcs.TYPES.2022.6},
  annote =	{Keywords: Dependent type theory, guarded recursion, modal type theory, proof assistants}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.22
Modular Verification of State-Based CRDTs in Separation Logic

Authors: Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Conflict-free Replicated Datatypes (CRDTs) are a class of distributed data structures that are highly-available and weakly consistent. The CRDT taxonomy is further divided into two subclasses: state-based and operation-based (op-based). Recent prior work showed how to use separation logic to verify convergence and functional correctness of op-based CRDTs while (a) verifying implementations (as opposed to high-level protocols), (b) giving high level specifications that abstract from low-level implementation details, and (c) providing specifications that are modular (i.e. allow client code to use the CRDT like an abstract data type). We extend this separation logic approach to verification of CRDTs to handle state-based CRDTs, while respecting the desiderata (a)-(c). The key idea is to track the state of a CRDT as a function of the set of operations that produced that state. Using the observation that state-based CRDTs are automatically causally-consistent, we obtain CRDT specifications that are agnostic to whether a CRDT is state- or op-based. When taken together with prior work, our technique thus provides a unified approach to specification and verification of op- and state-based CRDTs. We have tested our approach by verifying StateLib, a library for building state-based CRDTs. Using StateLib, we have further verified convergence and functional correctness of multiple example CRDTs from the literature. Our proofs are written in the Aneris distributed separation logic and are mechanized in Coq.
Cite as

Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal. Modular Verification of State-Based CRDTs in Separation Logic. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 22:1-22:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{nieto_et_al:LIPIcs.ECOOP.2023.22,
  author =	{Nieto, Abel and Daby-Seesaram, Arnaud and Gondelman, L\'{e}on and Timany, Amin and Birkedal, Lars},
  title =	{{Modular Verification of State-Based CRDTs in Separation Logic}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{22:1--22:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.22},
  URN =		{urn:nbn:de:0030-drops-182154},
  doi =		{10.4230/LIPIcs.ECOOP.2023.22},
  annote =	{Keywords: separation logic, distributed systems, CRDT, replicated data type, formal verification}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.15
Modular Verification of State-Based CRDTs in Separation Logic (Artifact)

Authors: Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
This is the documentation of the artifact for the paper "Modular Verification of State-Based CRDTs in Separation Logic". The artifact consists of a Coq formalization of the safety proofs for state-based CRDTs described in the paper. The Coq proofs are written in the Aneris distributed separation logic.
Cite as

Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal. Modular Verification of State-Based CRDTs in Separation Logic (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 15:1-15:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{nieto_et_al:DARTS.9.2.15,
  author =	{Nieto, Abel and Daby-Seesaram, Arnaud and Gondelman, L\'{e}on and Timany, Amin and Birkedal, Lars},
  title =	{{Modular Verification of State-Based CRDTs in Separation Logic (Artifact)}},
  pages =	{15:1--15:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Nieto, Abel and Daby-Seesaram, Arnaud and Gondelman, L\'{e}on and Timany, Amin and Birkedal, Lars},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.9.2.15},
  URN =		{urn:nbn:de:0030-drops-182553},
  doi =		{10.4230/DARTS.9.2.15},
  annote =	{Keywords: separation logic, distributed systems, CRDT, replicated data type, formal verification}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.23
A Stratified Approach to Löb Induction

Authors: Daniel Gratzer and Lars Birkedal

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Guarded type theory extends type theory with a handful of modalities and constants to encode productive recursion. While these theories have seen widespread use, the metatheory of guarded type theories, particularly guarded dependent type theories remains underdeveloped. We show that integrating Löb induction is the key obstruction to unifying guarded recursion and dependence in a well-behaved type theory and prove a no-go theorem sharply bounding such type theories. Based on these results, we introduce GuTT: a stratified guarded type theory. GuTT is properly two type theories, sGuTT and dGuTT. The former contains only propositional rules governing Löb induction but enjoys decidable type-checking while the latter extends the former with definitional equalities. Accordingly, dGuTT does not have decidable type-checking. We prove, however, a novel guarded canonicity theorem for dGuTT, showing that programs in dGuTT can be run. These two type theories work in concert, with users writing programs in sGuTT and running them in dGuTT.
Cite as

Daniel Gratzer and Lars Birkedal. A Stratified Approach to Löb Induction. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 23:1-23:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gratzer_et_al:LIPIcs.FSCD.2022.23,
  author =	{Gratzer, Daniel and Birkedal, Lars},
  title =	{{A Stratified Approach to L\"{o}b Induction}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{23:1--23:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.23},
  URN =		{urn:nbn:de:0030-drops-163048},
  doi =		{10.4230/LIPIcs.FSCD.2022.23},
  annote =	{Keywords: Dependent type theory, guarded recursion, modal type theory, canonicity, categorical gluing}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.23
Guarded Cubical Type Theory: Path Equality for Guarded Recursion

Authors: Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Löf type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, is conjectured to have decidable type checking, and has an implemented type checker. Our new type theory, called guarded cubical type theory, provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation, and present semantics in a presheaf category.
Cite as

Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{birkedal_et_al:LIPIcs.CSL.2016.23,
  author =	{Birkedal, Lars and Bizjak, Ale\v{s} and Clouston, Ranald and Grathwohl, Hans Bugge and Spitters, Bas and Vezzosi, Andrea},
  title =	{{Guarded Cubical Type Theory: Path Equality for Guarded Recursion}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.23},
  URN =		{urn:nbn:de:0030-drops-65638},
  doi =		{10.4230/LIPIcs.CSL.2016.23},
  annote =	{Keywords: Guarded Recursion, Dependent Type Theory, Cubical Type Theory, Denotational Semantics, Homotopy Type Theory}
}
Document
DOI: 10.4230/DagRep.5.5.1
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191)

Authors: Lars Birkedal, Derek Dreyer, Philippa Gardner, and Zhong Shao

Published in: Dagstuhl Reports, Volume 5, Issue 5 (2016)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15191 "Compositional Verification Methods for Next-Generation Concurrency". The seminar was successful and facilitated a stimulating interchange between the theory and practice of concurrent programming, and thereby laid the ground for the development of compositional verification methods that can scale to handle the realities of next-generation concurrency.
Cite as

Lars Birkedal, Derek Dreyer, Philippa Gardner, and Zhong Shao. Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). In Dagstuhl Reports, Volume 5, Issue 5, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{birkedal_et_al:DagRep.5.5.1,
  author =	{Birkedal, Lars and Dreyer, Derek and Gardner, Philippa and Shao, Zhong},
  title =	{{Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191)}},
  pages =	{1--23},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{5},
  editor =	{Birkedal, Lars and Dreyer, Derek and Gardner, Philippa and Shao, Zhong},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.5.1},
  URN =		{urn:nbn:de:0030-drops-53565},
  doi =		{10.4230/DagRep.5.5.1},
  annote =	{Keywords: Verification of Concurrent Programs (Models, Logics, Automated Analysis), Concurrent Programming}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.107
A Concurrent Logical Relation

Authors: Lars Birkedal, Filip Sieczkowski, and Jacob Thamsborg

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
We present a logical relation for showing the correctness of program transformations based on a new type-and-effect system for a concurrent extension of an ML-like language with higher-order functions, higher-order store and dynamic memory allocation. We show how to use our model to verify a number of interesting program transformations that rely on effect annotations. In particular, we prove a Parallelization Theorem, which expresses when it is sound to run two expressions in parallel instead of sequentially. The conditions are expressed solely in terms of the types and effects of the expressions. To the best of our knowledge, this is the first such result for a concurrent higher-order language with higher-order store and dynamic memory allocation.
Cite as

Lars Birkedal, Filip Sieczkowski, and Jacob Thamsborg. A Concurrent Logical Relation. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 107-121, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{birkedal_et_al:LIPIcs.CSL.2012.107,
  author =	{Birkedal, Lars and Sieczkowski, Filip and Thamsborg, Jacob},
  title =	{{A Concurrent Logical Relation}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{107--121},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.107},
  URN =		{urn:nbn:de:0030-drops-36671},
  doi =		{10.4230/LIPIcs.CSL.2012.107},
  annote =	{Keywords: verification, logical relation, concurrency, type and effect system}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.512
Step-Indexed Relational Reasoning for Countable Nondeterminism

Authors: Jan Schwinghammer and Lars Birkedal

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
Programming languages with countable nondeterministic choice are computationally interesting since countable nondeterminism arises when modeling fairness for concurrent systems. Because countable choice introduces non-continuous behaviour, it is well-known that developing semantic models for programming languages with countable nondeterminism is challenging. We present a step-indexed logical relations model of a higher-order functional programming language with countable nondeterminism and demonstrate how it can be used to reason about contextually defined may- and must-equivalence. In earlier step-indexed models, the indices have been drawn from omega. Here the step-indexed relations for must-equivalence are indexed over an ordinal greater than omega.
Cite as

Jan Schwinghammer and Lars Birkedal. Step-Indexed Relational Reasoning for Countable Nondeterminism. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 512-524, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{schwinghammer_et_al:LIPIcs.CSL.2011.512,
  author =	{Schwinghammer, Jan and Birkedal, Lars},
  title =	{{Step-Indexed Relational Reasoning for Countable Nondeterminism}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{512--524},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.512},
  URN =		{urn:nbn:de:0030-drops-32535},
  doi =		{10.4230/LIPIcs.CSL.2011.512},
  annote =	{Keywords: countable choice, lambda calculus, program equivalence}
}
Document
DOI: 10.4230/DagSemProc.10351.1
10351 Abstracts Collection – Modelling, Controlling and Reasoning About State

Authors: Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract
From 29 August 2010 to 3 September 2010, the Dagstuhl Seminar 10351 ``Modelling, Controlling and Reasoning About State '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. Links to extended abstracts or full papers are provided, if available.
Cite as

Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann. 10351 Abstracts Collection – Modelling, Controlling and Reasoning About State. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ahmed_et_al:DagSemProc.10351.1,
  author =	{Ahmed, Amal and Benton, Nick and Birkedal, Lars and Hofmann, Martin},
  title =	{{10351 Abstracts Collection – Modelling, Controlling and Reasoning About State}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--16},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.1},
  URN =		{urn:nbn:de:0030-drops-28116},
  doi =		{10.4230/DagSemProc.10351.1},
  annote =	{Keywords: Mutable State, Program Logics, Semantics, Type Systems, Verification}
}
Document
DOI: 10.4230/DagSemProc.10351.2
10351 Executive Summary – Modelling, Controlling and Reasoning About State

Authors: Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract
From 29 August 2010 to 3 September 2010, the Dagstuhl Seminar 10351 ``Modelling, Controlling and Reasoning About State '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. 44 researchers, with interests and expertise in many different aspects of modelling and reasoning about mutable state, met to present their current work and discuss ongoing projects and open problems. This executive summary provides a general overview of the goals of the seminar and of the topics discussed.
Cite as

Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann. 10351 Executive Summary – Modelling, Controlling and Reasoning About State. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ahmed_et_al:DagSemProc.10351.2,
  author =	{Ahmed, Amal and Benton, Nick and Birkedal, Lars and Hofmann, Martin},
  title =	{{10351 Executive Summary – Modelling, Controlling and Reasoning About State}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.2},
  URN =		{urn:nbn:de:0030-drops-28108},
  doi =		{10.4230/DagSemProc.10351.2},
  annote =	{Keywords: Mutable State, Program Logics, Semantics, Type Systems, Verification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact